BEGIN

EVAL '(DECLARE (DECIMAL) (SPECIAL AXIOMS CURLIN CURPRF PROOFS SCHEMAS THEOREMS) (SPECIAL LOGICALCONSTANTS 
	QUANTIFIERS) (SPECIAL EXPEXP EXPLGTH EXPLIM ORDCNT) (SPECIAL CONSOLEWIDTH DDWIDTH FILEWIDTH IIIWIDTH 
	IMLACWIDTH TTYWIDTH) (SPECIAL ?*FILEPRINT PRECLIS?* ?*PRINT ?*TWODIM));


MACRO FIRSTPROP (L);
	'CDR CONS CDR L;


MACRO LASTPROP (L);
	'NULL CONS CDR L;


MACRO NEXTPROP (L);
	'CDDR CONS CDR L;


MACRO PROPNAM (L);
	'CAR CONS CDR L;


MACRO PROPTABLE (L);
	'CDR CONS CDR L;


MACRO PROPVAL (L);
	'CADR CONS CDR L;


EXPR DELETEPROP (IDENT, PROPNAM);
	BEGIN
	NEW TEM;
	TEM ← IDENT;
LOOP; 	IF NULL CDR TEM THEN RETURN NIL;
	IF TEM[2] EQ PROPNAM THEN RETURN PROG2(RPLACD(TEM, CDDDR TEM), T);
	TEM ← CDDR TEM;
	GO LOOP;
	END;


EXPR GETGET (ATOM, PROP);
	BEGIN
	NEW TEM, PTAB;
	PTAB ← CDR ATOM;
LOOP; 	IF NULL PTAB THEN RETURN NIL;
	TEM ← SEEKPROP(CAR PTAB, PROP);
	IF ¬NULL TEM THEN RETURN TEM;
	PTAB ← CDDR PTAB;
	GO LOOP;
	END;


EXPR INITPROP (IDENT, VALUE, NAME);
	RPLACD(IDENT, NAME CONS VALUE CONS CDR IDENT);


EXPR SEEKPROP (IDENT, PROPNAM);
	BEGIN
	NEW TEM;
	TEM ← GETL(IDENT, <PROPNAM>);
	IF NULL TEM THEN RETURN NIL;
	RETURN TEM;
	END;


FEXPR AE (ARGS);
	BEGIN
	NEW WFF;
	WFF ← WFFPART(CAR ARGS);
	IF CAR WFF ≠ 'AND THEN ERREND('(FIRST ARG IS NOT AN AND));
	ADDLINE(ANDELIM1(WFF, CDR ARGS), 'AE CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR AI (ARGS);
	ADDLINE(CONJOIN(WFFLIST(ARGS)), 'AI CONS ARGS, UNION(ASSLIST(ARGS)));


FEXPR ALT (ARGS);
	BEGIN
	NEW NEWEXP;
	NEWEXP ← ALT1(WFFPART(CAR ARGS), WFFPART(ARGS[2]));
	IF ¬VALID(NEWEXP) THEN ERREND('(LINES ARE NOT ALTERNATIVES));
	ADDLINE(NEWEXP, <'ALT CONS ARGS>, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR ASS (PROP);
	ADDLINE(CAR PROP, 'ASS CONS PROP, <NEXTLINE()>);


FEXPR BS (ARGS);
	ADDLINE(BOUNDSUBST(WFFPART(CAR ARGS), MAKECONSES(CDR ARGS), NIL), 'BS CONS ARGS, ASSPART(CAR ARGS));


FEXPR DED (LINES);
	BEGIN
	IF NULL LINES THEN ERREND('(NOTHING TO CONCLUDE));
	ADDLINE(<'IMPLIES, CONJOIN(WFFLIST(CDR LINES)), WFFPART(CAR LINES)>, 'DED CONS LINES, SETDIF(ASSPART(
		CAR LINES), CDR LINES));
	END;


FEXPR DEF (ARGS);
	BEGIN
	IF ¬ATOM CAR ARGS THEN ERREND('(NAMES MUST BE ATOMS));
	ADDLINE('SETQ CONS ARGS, 'DEF CONS ARGS, <NEXTLINE()>);
	END;


FEXPR DNE (LINE);
	BEGIN
	NEW NEWSTAT;
	IF ¬VALID(NEWSTAT ← DOUBLENEG(WFFPART(CAR LINE))) THEN ERREND('(NO DOUBLE NEGATIVE));
	ADDLINE(NEWSTAT, 'DNE CONS LINE, ASSPART(CAR LINE));
	END;


FEXPR DNI (LINE);
	ADDLINE(<'NOT, <'NOT, WFFPART(CAR LINE)>>, 'DNI CONS LINE, ASSPART(CAR LINE));


FEXPR EG (ARGS);
	ADDLINE(EXGEN1(WFFPART(CAR ARGS), CDR ARGS), 'EG CONS ARGS, ASSPART(CAR ARGS));


FEXPR ELIM (ARGS);
	BEGIN
	NEW NEW;
	NEW ← WFFPART(ARGS[2]);
	IF CAR NEW ≠ 'SETQ THEN ERREND('(NO DEFINITION));
	ADDLINE(SUBST(NEW[3], NEW[2], WFFPART(CAR ARGS)), 'ELIM CONS ARGS, SETDIF(ASSPART(CAR ARGS), ASSPART(
		ARGS[2])));
	END;


FEXPR EQE (ARGS);
	BEGIN
	NEW NEW;
	NEW ← WFFPART(CAR ARGS);
	IF CAR NEW ≠ 'EQUIVALENT THEN ERREND('(NO EQUIVALENCE));
	NEW ← 	IF ARGS[2] = 2 THEN REVERSE CDR NEW
		ELSE CDR NEW;
	ADDLINE('IMPLIES CONS NEW, 'EQE CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR EQI (ARGS);
	BEGIN
	NEW NEW;
	IF ¬VALID(NEW ← EQI1(WFFPART(CAR ARGS), WFFPART(CAR ARGS))) THEN ERREND('(ARE NOT EQUIVALENT));
	ADDLINE(NEW, 'EQI CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR ES (ARGS);
	ADDLINE(SPECALL(WFFPART(CAR ARGS), CDR ARGS), 'ES CONS ARGS, ASSPART(CAR ARGS));


FEXPR IFE (ARGS);
	BEGIN
	NEW NEW;
	IF ¬VALID(NEW ← IFE1(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN 
		ERREND('(NO IF ?- THEN ?- ELSE EXPRESSION));
	ADDLINE(NEW, 'IFE CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR IFI (ARGS);
	BEGIN
	NEW NEW;
	IF ¬VALID(NEW ← IFI1(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN 
		ERREND('(NEED IMPLICATIONS WITH OPPOSITE ANTECEDENTS));
	ADDLINE(NEW, 'IFI CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR LC (ARGS);
	ADDLINE(<'EQUAL, ARGS, LAMEXP(ARGS)>, 'LC CONS ARGS, NIL);


FEXPR MP (ARGS);
	BEGIN
	NEW NEWSTAT;
	IF ¬VALID(NEWSTAT ← MP1(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN 
		ERREND('(CANNOT MODUS PONENS));
	ADDLINE(NEWSTAT, 'MP CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR NE (ARGS);
	BEGIN
	IF ¬VALID(NOTELIM(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN ERREND('(NO CONTRADICTION));
	ADDLINE('FALSE, 'NE CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR NI (IM);
	BEGIN
	NEW NEWSTAT;
	IF ¬VALID(NEWSTAT ← NOTINTRO(WFFPART(CAR IM))) THEN ERREND('(NO IMPLIES FALSE));
	ADDLINE(NEWSTAT, 'NI CONS IM, ASSPART(CAR IM));
	END;


FEXPR OE (ARGS);
	BEGIN
	IF NULL ARGS | NULL CDR ARGS THEN ERREND('(NEED AT LEAST TWO ARGS));
	ADDLINE(ORELIM1(WFFPART(CAR ARGS), WFFLIST(CDR ARGS)), 'OE CONS ARGS, UNION(ASSLIST(ARGS)));
	END;


FEXPR OI (ARGS);
	BEGIN
	NEW KNOWN, SAVARGS, WFFS;
	SAVARGS ← ARGS;
LOOP; 	IF NULL ARGS THEN 
		IF NULL KNOWN THEN ERREND('(NO VALID PROPOSITION))
		ELSE GO ADDL;
	IF NUMBERP CAR ARGS THEN 
		(IF NULL KNOWN THEN KNOWN ← CAR ARGS);
	IF NUMBERP CAR ARGS THEN WFFS ← WFFPART(CAR ARGS) CONS WFFS
	ELSE WFFS ← CAR ARGS CONS WFFS;
	ARGS ← CDR ARGS;
	GO LOOP;
ADDL; 	ADDLINE(IF NULL CDR WFFS THEN CAR WFFS
		ELSE 'OR CONS REVERSE WFFS, 'OI CONS SAVARGS, ASSPART(KNOWN));
	END;


FEXPR REP (ARGS);
	BEGIN
	NEW NEW;
	NEW ← WFFPART(ARGS[2]);
	IF ¬ISEQUIVALENCE(CAR NEW) THEN ERREND('(NO EQUATION));
	NEW ← 	IF ARGS[3] = 2 THEN REVERSE CDR NEW
		ELSE CDR NEW;
	ADDLINE(SUBST(NEW[2], CAR NEW, WFFPART(CAR ARGS)), 'REP CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(
		ARGS[2])));
	END;


FEXPR REPL (ARGS);
	ADDLINE(REPEITHER(WFFPART(CAR ARGS), WFFPART(ARGS[2]), T, ARGS[3]), 'REPL CONS ARGS, UNION2(ASSPART(CAR
		 ARGS), ASSPART(ARGS[2])));


FEXPR REPR (ARGS);
	ADDLINE(REPEITHER(WFFPART(CAR ARGS), WFFPART(ARGS[2]), NIL, ARGS[3]), 'REPR CONS ARGS, UNION2(ASSPART
		(CAR ARGS), ASSPART(ARGS[2])));


FEXPR TAUT (L);
	BEGIN
	IF ¬TH1(NIL, NIL, WFFLIST(CDR L), <CAR L>) THEN ERREND('(DOES NOT FOLLOW));
	ADDLINE(CAR L, 'TAUT CONS L, UNION(ASSLIST(CDR L)));
	END;


FEXPR UG (ARGS);
	BEGIN
	NEW ASS, VARS, WFF;
	WFF ← WFFPART(CAR ARGS);
	ASS ← ASSPART(CAR ARGS);
	VARS ← CDR ARGS;
LOOP; 	IF NULL VARS THEN GO ADDL;
	IF ATOM CAR VARS THEN GO ATOM;
	IF VARS[1,1] = 'CONS THEN GO DOT;
	ERREND('(ILLEGAL ARGUMENT));
ATOM; 	WFF ← UNGEN(WFF, ASS, CAR VARS, CAR VARS);
	GO ELOOP;
DOT; 	WFF ← UNGEN(WFF, ASS, VARS[1,2], VARS[1,3]);
ELOOP; 	VARS ← CDR VARS;
	GO LOOP;
ADDL; 	ADDLINE(WFF, 'UG CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR US (ARGS);
	BEGIN
	ADDLINE(SPECALL(WFFPART(CAR ARGS), CDR ARGS), 'US CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR USEAX (ARGS);
	BEGIN
	NEW AX, FORM;
	AX ← GET(CAR ARGS, 'AXIOM);
	IF NULL AX THEN ERREND('(NO SUCH AXIOM));
	FORM ← SPECALL(AX, CDR ARGS);
	ADDLINE(FORM, 'USEAX CONS ARGS, NIL);
	END;


FEXPR USESCHM (ARGS);
	BEGIN
	NEW SCHEMA;
	SCHEMA ← GET(CAR ARGS, 'SCHEMA);
	IF NULL SCHEMA THEN ERREND('(IS NOT SCHEMA));
	ADDLINE(LAMEXP(PROPSUBST(ARGS[2], SCHEMA[1,2], SCHEMA[2])), 'USESCHM CONS ARGS, NIL);
	END;


FEXPR USETHM (ARGS);
	BEGIN
	NEW TH, FORM;
	TH ← GET(CAR ARGS, 'THEOREM);
	IF NULL TH THEN ERREND('(NO SUCH THEOREM));
	FORM ← SPECALL(TH, CDR ARGS);
	ADDLINE(FORM, 'USETHM CONS ARGS, NIL);
	END;


FEXPR BT (LINO);
	BEGIN
	NEW PROOF;
	LINO ← 	IF NULL LINO THEN CURLINE() - 1
		ELSE CAR LINO;
	PROOF ← CURTEXT();
	IF LINO ?*GREAT CURLINE() | LINO ?*LESS 0 THEN ERREND('(NON EXISTANT LINE));
	IF LINO = 0 THEN PUTPROP(CURPROOF(), NIL, 'PROOF)
	ELSE 	BEGIN
		RPLACD(NTHCDR(PROOF, LINO - 1), NIL);
		PUTPROP(CURPROOF(), PROOF, 'PROOF);
		END;
	INITPROOF(CURPROOF());
	SHOWCURLINE();
	END;


FEXPR FINDL (L);
	BEGIN
	NEW PRF, TXT, WFF;
	WFF ← CAR L;
	PRF ← 	IF ¬NULL CDR L THEN L[2]
		ELSE CURPROOF();
	TXT ← GET(PRF, 'PROOF);
LOOP; 	IF NULL TXT THEN RETURN NIL;
	IF WFF = TXT[1,2] THEN SHOWLINE(CAR TXT);
	TXT ← CDR TXT;
	GO LOOP;
	END;


FEXPR GIVEAX (L);
	BEGIN
	IF ¬ATOM CAR L THEN ERREND('(NON ATOMIC AXIOM NAME));
	IF ¬(CAR L ε AXIOMS) THEN AXIOMS ← AXIOMS @ <CAR L>;
	PUTPROP(CAR L, L[2], 'AXIOM);
	IF ?*PRINT THEN SHOWAXIOM(CAR L);
	END;


FEXPR GIVESCHM (L);
	BEGIN
	IF ¬ATOM CAR L THEN ERREND('(NON ATOMIC SCHEMA NAME));
	IF ¬(CAR L ε SCHEMAS) THEN SCHEMAS ← SCHEMAS @ <CAR L>;
	PUTPROP(CAR L, L[2], 'SCHEMA);
	IF ?*PRINT THEN SHOWSCHEMA(CAR L);
	END;


EXPR INVENTORY ();
	BEGIN
	IF ¬NULL AXIOMS THEN 
		BEGIN
		TERPRI();
		PRINT 'AXIOMS;
		PRINL(AXIOMS);
		END;
	IF ¬NULL SCHEMAS THEN 
		BEGIN
		TERPRI();
		PRINT 'SCHEMAS;
		PRINL(SCHEMAS);
		END;
	IF ¬NULL PROOFS THEN 
		BEGIN
		TERPRI();
		PRINT 'PROOFS;
		PRINL(PROOFS);
		END;
	IF ¬NULL THEOREMS THEN 
		BEGIN
		TERPRI();
		PRINT 'THEOREMS;
		PRINL(THEOREMS);
		END;
	END;


FEXPR MAKETHM (ARG);
	MAKETHEOREM1(CAR ARG, ARG[2], 
		IF ¬NULL CDDR ARG THEN ARG[3]
		ELSE CURPROOF());


EXPR ONDD ();
	BEGIN
	INITSTANCHARSET();
	LINELENGTH (CONSOLEWIDTH ← DDWIDTH);
	END;


EXPR ONIII ();
	BEGIN
	INITSTANCHARSET();
	LINELENGTH (CONSOLEWIDTH ← IIIWIDTH);
	END;


EXPR ONIMLAC ();
	BEGIN
	INITSTANCHARSET();
	LINELENGTH (CONSOLEWIDTH ← IMLACWIDTH);
	END;


EXPR ONTTY ();
	BEGIN
	INITTTYCHARSET();
	LINELENGTH (CONSOLEWIDTH ← TTYWIDTH);
	END;


FEXPR PROOF (NAME);
	BEGIN
	IF NULL NAME THEN ERREND('(NO NAME GIVEN));
	IF ¬ATOM CAR NAME THEN ERREND('(NON ATOMIC PROOF NAME));
	INITPROOF(CAR NAME);
	IF ?*PRINT THEN SHOWCURLINE();
	END;


FEXPR REDO (ARGS);
	BEGIN
	NEW CHANGED, CURL, LASTL, NEWC;
	IF WFFPART(CAR ARGS) ≠ WFFPART(ARGS[2]) THEN ERREND('(CANNOT REDO));
	CHANGED ← (CAR ARGS CONS ARGS[2]) CONS NIL;
	CURL ← CAR ARGS + 1;
	LASTL ← CURLINE() + 1;
LOOP; 	IF CURL EQ LASTL THEN RETURN NIL;
	NEWC ← SUBLIS(CHANGED, BYPART(CURL));
	IF NEWC = BYPART(CURL) THEN GO ELOOP
	ELSE EVAL NEWC;
	CHANGED ← (CURL CONS CURLINE()) CONS CHANGED;
ELOOP; 	CURL ← CURL + 1;
	GO LOOP;
	END;


FEXPR RESTOREALL (FILES);
	BEGIN
	NEW DEV, FILE, ?*PRINT;
	IF ?*FILEPRINT THEN 
		BEGIN
		?*PRINT ← T;
		END;
	DEV ← 'DSK;
LOOP; 	IF NULL FILES THEN GO EXIT;
	FILE ← CAR FILES;
	IF ATOM FILE THEN GO READ;
	IF CAR FILE = 'QUOTE THEN GO DEVICE;
	IF CAR FILE = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE OR DEVICE NAME));
READ; 	READIN(DEV, <FILE>, NIL);
	GO ELOOP;
DOTTED; 	FILE ← FILE[2] CONS FILE[3];
	GO READ;
DEVICE; 	DEV ← FILE[2];
	GO ELOOP;
ELOOP; 	FILES ← CDR FILES;
	GO LOOP;
EXIT; 	INVENTORY();
	END;


FEXPR SAVEALL (FILE);
	BEGIN
	NEW DEV, ITEM;
	DEV ← 'DSK;
LOOP; 	IF NULL FILE THEN ERREND('(DEVICE BUT NO FILE));
	ITEM ← CAR FILE;
	IF ATOM ITEM THEN GO OUTPUT;
	IF CAR ITEM = 'QUOTE THEN GO DEVICE;
	IF CAR ITEM = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE SPECIFIER));
DEVICE; 	DEV ← ITEM[2];
	FILE ← CDR FILE;
	GO LOOP;
DOTTED; 	ITEM ← ITEM[2] CONS ITEM[3];
OUTPUT; 	EVAL <'OUTPUT, DEV, ITEM>;
	OUTC(T, NIL);
	LINELENGTH FILEWIDTH;
	MAPC(FUNCTION(SAVEAXIOM), AXIOMS);
	MAPC(FUNCTION(SAVESCHEMA), SCHEMAS);
	MAPC(FUNCTION(SAVEPROOF), PROOFS);
	MAPC(FUNCTION(SAVETHEOREM), THEOREMS);
	OUTC(NIL, T);
	INVENTORY();
	END;


FEXPR SAVECOMS (FILE);
	BEGIN
	NEW DEV, ITEM;
	DEV ← 'DSK;
LOOP; 	IF NULL FILE THEN ERREND('(NO FILE SPECIFIED));
	ITEM ← CAR FILE;
	IF ATOM ITEM THEN GO OUTPUT;
	IF CAR ITEM = 'QUOTE THEN GO DEVICE;
	IF CAR ITEM = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE SPECIFIER));
DEVICE; 	DEV ← ITEM[2];
	FILE ← CDR FILE;
	GO LOOP;
DOTTED; 	ITEM ← ITEM[2] CONS ITEM[3];
OUTPUT; 	EVAL <'OUTPUT, DEV, ITEM>;
	OUTC(T, NIL);
	LINELENGTH FILEWIDTH;
	MAPC(FUNCTION(SAVEAXCOM), AXIOMS);
	MAPC(FUNCTION(SAVESCHMCOM), SCHEMAS);
	MAPC(FUNCTION(SAVEPRFCOM), PROOFS);
	MAPC(FUNCTION(SAVETHMCOM), THEOREMS);
	OUTC(NIL, T);
	INVENTORY();
	END;


FEXPR SHOW (THINGS);
	BEGIN
	NEW LINE1, LINE2, TEM;
TOP; 	IF NULL THINGS THEN RETURN SHOWPROOF(CURPROOF());
LOOP; 	IF NULL THINGS THEN GO EXIT;
	IF ¬ATOM CAR THINGS THEN GO DEV;
	IF NUMBERP CAR THINGS THEN GO LINES;
	TEM ← GETGET(CAR THINGS, 'IMAGE);
	IF NULL TEM THEN ERREND('(NOTHING TO SHOW));
	EVAL '((CADR TEM) (CAR THINGS));
ELOOP; 	THINGS ← CDR THINGS;
	GO LOOP;
LINES; 	LINE1 ← CAR THINGS;
	THINGS ← CDR THINGS;
	IF NULL THINGS | ¬NUMBERP CAR THINGS THEN LINE2 ← LINE1
	ELSE 	BEGIN
		LINE2 ← CAR THINGS;
		THINGS ← CDR THINGS;
		END;
LLOOP; 	IF LINE1 ?*GREAT LINE2 THEN GO EXIT;
	SHOWLINE(GETLINE(LINE1));
	LINE1 ← LINE1 + 1;
	GO LLOOP;
DEV; 	IF THINGS[1,1] ≠ 'QUOTE THEN ERREND('(NEED NAME OR FILE SPEC));
	EVAL ('OUTPUT CONS THINGS[1,2]);
	OUTC(T, T);
	THINGS ← CDR THINGS;
	GO TOP;
EXIT; 	OUTC(NIL, T);
	END;


FEXPR SHOWALL (FILE);
	BEGIN
	NEW DEV, ITEM;
	DEV ← 'DSK;
LOOP; 	IF NULL FILE THEN ERREND('(NO FILE SPECIFIED));
	ITEM ← CAR FILE;
	IF ATOM ITEM THEN GO OUTPUT;
	IF CAR ITEM = 'QUOTE THEN GO DEVICE;
	IF CAR ITEM = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE SPECIFIER));
DEVICE; 	DEV ← ITEM[2];
	FILE ← CDR FILE;
	GO LOOP;
DOTTED; 	ITEM ← ITEM[2] CONS ITEM[3];
OUTPUT; 	EVAL <'OUTPUT, DEV, ITEM>;
	OUTC(T, NIL);
	LINELENGTH FILEWIDTH;
	MAPC(FUNCTION(SHOWAXIOM), AXIOMS);
	MAPC(FUNCTION(SHOWSCHEMA), SCHEMAS);
	MAPC(FUNCTION(SHOWPROOF), PROOFS);
	MAPC(FUNCTION(SHOWTHEOREM), THEOREMS);
	OUTC(NIL, T);
	INVENTORY();
	END;


FEXPR SSEX (L);
	BEGIN
	NEW LINE, NAME, PRF;
	NAME ← 	IF NULL L THEN CURPROOF()
		ELSE CAR L;
	PRF ← GETL(NAME, '(PROOF));
	IF NULL PRF THEN ERREND('(NO PROOF BY THAT NAME));
	PRF ← PRF[2];
	PRINT 'PROOF;
	PRINS(NAME);
LOOP; 	IF NULL PRF THEN RETURN NIL;
	LINE ← CAR PRF;
	TERPRI();
	PRINC CAR LINE;
	PRINC '?/;
	PRINTSUBEXPR(LINE[2], CURCOL(), 0);
	IF FLATSIZE CDDR LINE + 6 ?*GREAT CHRCT() THEN GO MANY;
	PRINC '?/;
	PRINS('BY);
	PRINS(LINE[3]);
	IF ¬NULL LINE[4] THEN 
		BEGIN
		PRINS('ASS);
		PRIN1 LINE[4];
		END;
ELOOP; 	PRF ← CDR PRF;
	GO LOOP;
MANY; 	TERPRI();
	PRINTN('?/, 4);
	PRINC 'BY;
	PRINC '?/;
	PRINTSUBEXPR(LINE[3], CURCOL(), 0);
	IF NULL LINE[4] THEN GO ELOOP;
	TERPRI();
	PRINTN('?/, 4);
	PRINC 'ASS;
	PRINC '?/;
	PRINS(LINE[4]);
	GO ELOOP;
	END;


EXPR ADDLINE (WFF, JUST, ASS);
	BEGIN
	PUTPROP(CURPROOF(), CURTEXT() NCONC <<CURLINE() + 1, WFF, JUST, ASS>>, 'PROOF);
	CURLIN ← CURLIN + 1;
	PUTPROP('?@, CURLINE(), 'NEWNAM);
	IF ?*PRINT THEN SHOWCURLINE();
	END;


FEXPR ADDAXIOM (L);
	BEGIN
	PUTPROP(CAR L, L[2], 'AXIOM);
	AXIOMS ← CAR L CONS AXIOMS;
	END;


FEXPR ADDSCHEMA (L);
	BEGIN
	PUTPROP(CAR L, L[2], 'SCHEMA);
	SCHEMAS ← CAR L CONS SCHEMAS;
	END;


FEXPR ADDTHEOREM (L);
	BEGIN
	PUTPROP(CAR L, L[2], 'THEOREM);
	THEOREMS ← CAR L CONS THEOREMS;
	END;


EXPR ALPHAPART (IDENT);
	BEGIN
	NEW CHARS;
	CHARS ← REVERSE EXPLODE IDENT;
LOOP; 	IF ¬NUMBERP CAR CHARS THEN RETURN READLIST REVERSE CHARS;
	CHARS ← CDR CHARS;
	GO LOOP;
	END;


EXPR ALLVARS (EXPRESSION);
	ALLVARS1(EXPRESSION, NIL);


EXPR ALLVARS1 (EXP, VARS);
	IF ATOM EXP THEN 
		IF ISVAR(EXP) THEN 
			IF EXP ε VARS THEN VARS
			ELSE EXP CONS VARS
		ELSE VARS
	ELSE ALLVARSL(CDR EXP, VARS);


EXPR ALLVARSL (EXPL, VARS);
	IF NULL EXPL THEN VARS
	ELSE ALLVARS1(CAR EXPL, ALLVARSL(CDR EXPL, VARS));


EXPR ALT1 (I1, I2);
	LAMBDA (U, V); 
		IF VALID(U) THEN SUBLIS(U, 'QQQ)
		ELSE IF VALID(V) THEN SUBLIS(V, 'QQQ)
		ELSE 'INVALID;
	(INST(I1 CONS I2, '((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ), NIL), INST(I2 CONS I1, '((IMPLIES PPP QQQ
		) IMPLIES (NOT PPP) QQQ), NIL));


EXPR ANDELIM1 (WFF, PLACES);
	BEGIN
	NEW CHOSEN, LEN;
	LEN ← LENGTH CDR WFF;
	IF CAR WFF NEQ 'AND THEN ERREND('(FIRST ARG IS NOT AN AND));
LOOP; 	IF NULL PLACES THEN RETURN CONJOIN(REVERSE CHOSEN);
	IF CAR PLACES ?*GREAT LEN THEN ERREND('(TOO FEW CONJUNCTS));
	CHOSEN ← NTHELT(CDR WFF, CAR PLACES) CONS CHOSEN;
	PLACES ← CDR PLACES;
	GO LOOP;
	END;


EXPR ASSLIST (L);
	MAPCAR(FUNCTION(ASSPART), L);


EXPR ASSOCR (ITM, LST);
	BEGIN
LOOP; 	IF NULL LST THEN RETURN NIL;
	IF ITM EQ CDAR LST THEN RETURN CAR LST;
	LST ← CDR LST;
	GO LOOP;
	END;


EXPR ASSPART (LINE);
	GETLINE(LINE)[4];


EXPR BINAND (ARGS);
	IF NULL ARGS THEN '(AND TRUE TRUE)
	ELSE IF NULL CDR ARGS THEN <'AND, CAR ARGS, 'TRUE>
	ELSE IF NULL CDDR ARGS THEN 'AND CONS ARGS
	ELSE <'AND, CAR ARGS, BINAND(CDR ARGS)>;


EXPR BINOR (ARGS);
	IF NULL ARGS THEN '(OR FALSE FALSE)
	ELSE IF NULL CDR ARGS THEN <'OR, CAR ARGS, 'FALSE>
	ELSE IF NULL CDDR ARGS THEN 'OR CONS ARGS
	ELSE <'OR, CAR ARGS, BINOR(CDR ARGS)>;


EXPR BYPART (LINE);
	GETLINE(LINE)[3];


EXPR BOUNDSUBST (EXP, SUBS, BINDS);
	BEGIN
	NEW TEM;
	IF ATOM EXP THEN GO ATOM;
	IF ISQUANT(EXP[1,1]) THEN GO QUANT;
	RETURN BOUNDSUBSTL(EXP, SUBS, BINDS);
ATOM; 	IF ISCONST(EXP) THEN RETURN EXP;
	TEM ← ASSOC(EXP, BINDS);
	IF ¬NULL TEM THEN RETURN CDR TEM;
	TEM ← ASSOCR(EXP, BINDS);
	IF ¬NULL TEM THEN ERREND('(FREE VARIABLE CAPTURE));
	RETURN EXP;
QUANT; 	TEM ← ASSOC(EXP[1,2], SUBS);
	TEM ← 	IF ¬NULL TEM THEN CDR TEM
		ELSE EXP[1,2];
	IF ¬NULL ASSOCR(TEM, BINDS) THEN ERREND('(BOUND VARIABLE CAPTURE));
	RETURN <<EXP[1,1], TEM>, BOUNDSUBST(EXP[2], SUBS, (EXP[1,2] CONS TEM) CONS BINDS)>;
	END;


EXPR BOUNDSUBSTL (LST, SUBS, BINDS);
	IF NULL LST THEN NIL
	ELSE BOUNDSUBST(CAR LST, SUBS, BINDS) CONS BOUNDSUBSTL(CDR LST, SUBS, BINDS);


EXPR CONJOIN (WFFS);
	IF NULL WFFS THEN 'TRUE
	ELSE IF NULL CDR WFFS THEN CAR WFFS
	ELSE 'AND CONS WFFS;


EXPR CURCOL ();
	LINELENGTH NIL + (1 - CHRCT());


EXPR CURLINE ();
	PROG2(CURPROOF(), CURLIN);


EXPR CURPROOF ();
	IF NULL CURPRF THEN ERREND('(NO CURRENT PROOF))
	ELSE CURPRF;


EXPR CURTEXT ();
	GET(CURPROOF(), 'PROOF);


EXPR DOUBLENEG (PROP);
	LAMBDA (W); 
		IF ¬VALID(W) THEN 'INVALID
		ELSE SUBLIS(W, 'PPP);
	(INST(PROP, '(NOT (NOT PPP)), NIL));


EXPR EXGEN1 (WFF, VARS);
	BEGIN
LOOP; 	IF NULL VARS THEN RETURN WFF;
	IF ATOM CAR VARS THEN GO ATOM;
	IF VARS[1,1] = 'CONS THEN GO DOT;
	ERREND('(ILLEGAL ARGUMENT));
ATOM; 	WFF ← EXGEN(WFF, CAR VARS, CAR VARS);
	GO ELOOP;
DOT; 	WFF ← EXGEN(WFF, VARS[1,2], VARS[1,3]);
ELOOP; 	VARS ← CDR VARS;
	GO LOOP;
	END;


EXPR EXGEN (WFF, OLD, NEW);
	BEGIN
	NEW TEM;
	TEM ← GENSYM();
	WFF ← SUBST(TEM, OLD, WFF);
	IF NEW ε ALLVARS(WFF) THEN ERREND('(NEW VARIABLE CONFLICTS));
	RETURN <<'THEREEXISTS, NEW>, SUBST(NEW, TEM, WFF)>;
	END;


EXPR EQI1 (WFF1, WFF2);
	LAMBDA (W); 
		IF ¬VALID(W) THEN 'INVALID
		ELSE SUBLIS(W, '(EQUIVALENT PPP QQQ));
	(INST(WFF1 CONS WFF2, '((IMPLIES PPP QQQ) IMPLIES QQQ PPP), NIL));


EXPR ERREND (MESSAGE);
	BEGIN
	PRINT MESSAGE;
	ERR();
	END;


EXPR FREEIN (VAR, LINES);
	IF NULL LINES THEN NIL
	ELSE IF VAR ε FREEVARS(WFFPART(CAR LINES)) THEN T
	ELSE FREEIN(VAR, CDR LINES);


EXPR FREEVARS (EXPRESSION);
	FREEVARS1(NIL, NIL, EXPRESSION);


EXPR FREEVARS1 (BVARS, FVARS, EXP);
	IF ATOM EXP THEN 
		IF ISVAR(EXP) THEN 
			IF EXP ε BVARS THEN FVARS
			ELSE IF EXP ε FVARS THEN FVARS
			ELSE EXP CONS FVARS
		ELSE FVARS
	ELSE IF ATOM CAR EXP THEN FREEVARS2(BVARS, FVARS, CDR EXP)
	ELSE IF ATOM EXP[1,1] THEN 
		(IF EXP[1,1] ε '(FORALL THEREEXISTS) THEN 
			FREEVARS1(EXP[1,2] CONS BVARS, FVARS, EXP[3]))
	ELSE ERREND('(UNKNOWN NONATOMIC FUNCTION));


EXPR FREEVARS2 (BVARS, FVARS, EXPL);
	IF NULL EXPL THEN FVARS
	ELSE FREEVARS1(BVARS, FREEVARS2(BVARS, FVARS, CDR EXPL), CAR EXPL);


EXPR GETCURLINE ();
	GETLINE(CURLINE());


EXPR GETLINE (LINENO);
	BEGIN
	NEW TEM;
	TEM ← ASSOC(LINENO, CURTEXT());
	IF NULL TEM THEN ERREND('(NO SUCH LINE));
	RETURN TEM;
	END;


FEXPR GIVEPROOF (L);
	BEGIN
	IF ¬ATOM CAR L THEN ERREND('(NON ATOMIC PROOF NAME));
	IF ¬(CAR L ε PROOFS) THEN PROOFS ← PROOFS @ <CAR L>;
	PUTPROP(CAR L, L[2], 'PROOF);
	END;


EXPR IFE1 (WFF1, WFF2);
	LAMBDA (W, X, Y, Z); 
		IF VALID(W) THEN SUBLIS(W, 'QQQ)
		ELSE IF VALID(X) THEN SUBLIS(X, 'RRR)
		ELSE IF VALID(Y) THEN SUBLIS(Y, 'QQQ)
		ELSE IF VALID(Z) THEN SUBLIS(Z, 'RRR)
		ELSE 'INVALID;
	(INST(WFF1 CONS WFF2, '(PPP COND (PPP QQQ) (T RRR)), NIL), INST(WFF1 CONS WFF2, '((NOT PPP) COND (PPP 
		QQQ) (T RRR)), NIL), INST(WFF2 CONS WFF1, '(PPP COND (PPP QQQ) (T RRR)), NIL), INST(WFF2 CONS 
		WFF1, '((NOT PPP) COND (PPP QQQ) (T RRR)), NIL));


EXPR IFI1 (WFF1, WFF2);
	LAMBDA (W, X); 
		IF VALID(W) THEN SUBLIS(W, '(COND (PPP QQQ) (T RRR)))
		ELSE IF VALID(X) THEN SUBLIS(X, '(COND (PPP QQQ) (T RRR)))
		ELSE 'INVALID;
	(INST(WFF1 CONS WFF2, '((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR), NIL), INST(WFF2 CONS WFF1, '((IMPLIES
		 PPP QQQ) IMPLIES (NOT PPP) RRR), NIL));


EXPR INITALL ();
	BEGIN
	CURPRF ← NIL;
	AXIOMS ← NIL;
	THEOREMS ← NIL;
	PROOFS ← NIL;
	SCHEMAS ← NIL;
	END;


EXPR INITOPS ();
	BEGIN
	NEW INCR, OP, PREC, PRECLIS;
	PRECLIS ← '?*COMMA?* CONS 'SETQ CONS PRECLIS?*;
LOOP; 	IF NULL PRECLIS THEN RETURN NIL;
	OP ← CAR PRECLIS;
	PREC ← GET(OP, 'INFIX);
	INCR ← 	IF GET(OP, 'LEFT) THEN MINUS 1
		ELSE 1;
	PUTPROP(OP, <3 * PREC + INCR, 3 * PREC - INCR>, 'PREC);
	PRECLIS ← CDR PRECLIS;
	GO LOOP;
	END;


EXPR INITPRONF (NAME);
	BEGIN
	IF NULL NAME THEN ERREND('(NIL NOT ACCEPTABLE PROOF NAME));
	CURPRF ← NAME;
	IF GETL(NAME, '(PROOF)) THEN GO EXIST;
	PUTPROP(NAME, NIL, 'PROOF);
	PROOFS ← PROOFS @ <NAME>;
EXIST; 	CURLIN ← 
		IF NULL CURTEXT() THEN 0
		ELSE (LAST CURTEXT())[1,1];
	PUTPROP('?@, CURLINE(), 'NEWNAM);
	END;


EXPR INITSTANCHARSET ();
	BEGIN
	PUTPROP('AND, '?∧, 'INFXNAM);
	PUTPROP('CMAPS, '?→?→, 'INFXNAM);
	PUTPROP('?*COMMA?*, '?,, 'INFXNAM);
	PUTPROP('CONS, '?., 'INFXNAM);
	PUTPROP('CONTAINED, '?⊂, 'INFXNAM);
	PUTPROP('DIFFERENCE, '?-, 'INFXNAM);
	PUTPROP('EQUAL, '?=, 'INFXNAM);
	PUTPROP('EQUIVALENT, '?≡, 'INFXNAM);
	PUTPROP('EXPT, '?↑, 'INFXNAM);
	PUTPROP('FORALL, '?∀, 'INFXNAM);
	PUTPROP('GEQ, '?≥, 'INFXNAM);
	PUTPROP('GREATERP, '?>, 'INFXNAM);
	PUTPROP('IMPLIES, '?⊃, 'INFXNAM);
	PUTPROP('INTERSECTION, '?∩, 'INFXNAM);
	PUTPROP('LAMBDA, '?λ, 'INFXNAM);
	PUTPROP('LEQ, '?≤, 'INFXNAM);
	PUTPROP('LESSP, '?<, 'INFXNAM);
	PUTPROP('MAPS, '?→, 'INFXNAM);
	PUTPROP('MEMBER, '?ε, 'INFXNAM);
	PUTPROP('MINUS, '?-, 'INFXNAM);
	PUTPROP('NEQ, '?≠, 'INFXNAM);
	PUTPROP('NOT, '?¬, 'INFXNAM);
	PUTPROP('OR, '?∨, 'INFXNAM);
	PUTPROP('PLUS, '?+, 'INFXNAM);
	PUTPROP('PRODUCT, '?⊗, 'INFXNAM);
	PUTPROP('QUOTE, '?', 'INFXNAM);
	PUTPROP('QUOTIENT, '?/, 'INFXNAM);
	PUTPROP('SETQ, '?←, 'INFXNAM);
	PUTPROP('THEREEXISTS, '?∃, 'INFXNAM);
	PUTPROP('TIMES, '?*, 'INFXNAM);
	PUTPROP('UNION, '?∪, 'INFXNAM);
	END;


END.